es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, Q:({e:E| loc(e) = loc(e1)  Id }Prop).
(e:{e:E| loc(e) = loc(e1)  Id }. Dec(Q(e)))
 ([e1,e2]~([a,b].b = first e  a.Q(e))+  e1  e2  & Q(e2)) 

latex

Definitions

P & Q, (e <loc e'), P  Q, e  e' , e2 = first e  e1.P(e), x:A. B(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), [e1,e2]~([a,b].p(a;b))+, x(s), x:A. B(x), t  T, loc(e), Id, E, Prop, x. t(x), P  Q, x,y. t(x;y), ES, Dec(P), P  Q, P  Q, [e, e'], ||as||, AB, , ij, A, False, b, e@i. P(e), e[e1,e2).P(e), A & B, pred(e), first(e), as @ bs, {T}, SQType(T), 1of(t), True, T, Top, S  T, e[e1,e2).P(e)

Lemmas

non neg length, es-pplus-trivial, es-pred wf, es-pplus-partition, es-interval-non-zero, length-append, es-interval wf2, top wf, squash wf, true wf, not wf, assert wf, es-first wf, es-locl-iff, append wf, es-le-trans2, es-pred-locl, es-locl wf, es-interval-partition, es-next, decidable existse-between1, es-loc-pred, es-interval wf, length wf1, le wf, es-le-loc, nat wf, nat properties, ge wf, es-pplus wf, es-le wf, decidable wf, event system wf, es-pplus-le, es-first-since wf, es-E wf, Id wf, es-loc wf